$\forall$${\it xm}$:XM, $T$:Type, $P$:($T$$\rightarrow\mathbb{P}$). ($\exists$$a$:$T$. $P$($a$)) $\Rightarrow$ (($\in$$x$:$T$. $P$($x$)) $\in$ $T$)